\begin{tabbing}
ma{-}single{-}sends0($B$;$T$;$a$;$l$;${\it tg}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=with declarations \+
\\[0ex]ds:
\\[0ex]da:fpf{-}join(KindDeq;$a$ : $B$;rcv($l$,${\it tg}$) : $T$)
\\[0ex]$a$(v) sends $\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. $f$($v$)$\rangle$.nil s v on link $l$
\-
\end{tabbing}